\begin{tabbing}
fair{-}fifo\=\{i:l\}\+
\\[0ex]($w$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk.\+\+
\\[0ex]($\neg$(source($l$) = $i$ $\in$ Id)) $\Rightarrow$ (onlnk($l$;w{-}m($w$; $i$; $t$)) = [] $\in$ (w{-}Msg($w$) List)))
\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\uparrow$w{-}isnull($w$; w{-}a($w$; $i$; $t$)))
\\[0ex]$\Rightarrow$ \=((\=$\forall$$x$:Id.\+\+
\\[0ex]w{-}s($w$; $i$; ($t$+1); $x$) = ($\lambda$$q$.w{-}s($w$; $i$; $t$; $x$)($q$ + 1)) $\in$ $\mathbb{Q}\rightarrow$w{-}vartype($w$; $i$; $x$))
\-\\[0ex]\& w{-}m($w$; $i$; $t$) = [] $\in$ (w{-}Msg($w$) List)))
\-\-\\[0ex]\& (\=($\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk.\+
\\[0ex]($\uparrow$w{-}isrcvl($w$; $l$; w{-}a($w$; $i$; $t$)))
\\[0ex]$\Rightarrow$ \=(destination($l$) = $i$ $\in$ Id\+
\\[0ex]\& (\=($\parallel$w{-}queue($w$; $l$; $t$)$\parallel$ $\geq$ 1 )\+
\\[0ex]c$\wedge$ (hd(w{-}queue($w$; $l$; $t$)) = w{-}msg($w$; w{-}a($w$; $i$; $t$)) $\in$ w{-}Msg($w$)))))
\-\-\\[0ex]c$\wedge$ \=((\=$\forall$$l$:IdLnk, $t$:$\mathbb{N}$.\+\+
\\[0ex]$\exists$\=${\it t'}$:$\mathbb{N}$\+
\\[0ex](($t$ $\leq$ ${\it t'}$)
\\[0ex]\& (\=($\uparrow$w{-}isrcvl($w$; $l$; w{-}a($w$; destination($l$); ${\it t'}$)))\+
\\[0ex]$\vee$ (w{-}queue($w$; $l$; ${\it t'}$) = [] $\in$ (w{-}Msg($w$) List)))))
\-\-\-\\[0ex]\& w{-}machine{-}constraint($w$)
\\[0ex]\& w{-}atom{-}constraint\=\{i:l\}\+
\\[0ex]($w$)
\-\\[0ex]\& w{-}discrete{-}constraint($w$)))
\-\-\-
\end{tabbing}